the_es:ES, j:E.
isrcv(j)
 snds(lnk(j), before(sender(j),index(j))) = nil  (Msg on lnk(j)) List
 msgs(lnk(j);before(j)) = nil  Msg List 

latex

Definitions

mlnk(m), emsg(e), IdLnk, haslink(l;m), , T, True, P  Q, l[i], AB, A, False, {T}, (e <loc e'), i  j < k, (x  l), x:A. B(x), A & B, S  T, null(as), msgs(l;before(e')), Dec(P), P  Q, P  Q, P & Q, Msg, Prop, snds(l, before(e,n)), index(e), {i..j}, ||as||, sends(l;e), sender(e), (Msg on l), lnk(e), P  Q, b, isrcv(e), E, x:A. B(x), t  T, ES

Lemmas

event system wf, es-E wf, es-isrcv wf, assert wf, es-lnk wf, es-Msgl wf, es-sender wf, es-sends wf, length wf1, int seg wf, es-index wf, es-snds-index wf, es-msgs wf, assert of null, not functionality wrt iff, null wf, decidable assert, es-Msg wf, member-es-msgs, member exists, es-axioms, assert-es-haslnk, l member wf, es-locl wf, select wf, le wf, member-es-snds-index, haslink wf2, IdLnk wf, true wf, squash wf, mlnk wf2